#pragma once
#include "def.h"
int VarN = 0,LineN = 0;

/***
	初始化链表
	注：该链表有头节点
***/

LinkClause init(char filename[]){
	int t;
	char waste[40];
	for (int i = 0; i < 10; i++) {
		waste[i] = '\0';
	}
	LinkClause C = new Clause;//哨兵位
	C->L = NULL;
	C->length = 0;
	C->next = NULL;
	LinkClause cur = new Clause;//从句链表当前指针
	LinkList cur2 = NULL;//单句链表当前指针
	C->next = cur;
	FILE* fp = fopen(filename,"r");
	while(fscanf(fp,"%s",waste)){
		if(strcmp(waste,"p") == 0){
			break;
		}
	}
	fscanf(fp,"%s",waste);
	fscanf(fp,"%d%d",&VarN,&LineN);
	//printf("VarN = %d,LineN = %d\n", VarN, LineN);
	C->length = LineN;
	for(int i = 0;i < LineN;i++){
		cur->L = new List;
		cur->length = 0;
		cur->next = NULL;
		while(fscanf(fp,"%d",&t),t){
			if(cur->length == 0){
				cur->L->num = t;
				cur->L->next = NULL;
				cur2 = cur->L;
			}
			else{
				LinkList temp = new List;
				temp->next = NULL;
				temp->num = t;
				cur2->next = temp;
				cur2 = cur2->next;
			}
			
			cur->length++;
		}
		if(i!=LineN-1){
		cur->next = new Clause;
		cur = cur->next;
		}
	}
	//printf("init successful\n");
	AddHead(C);
	fclose(fp);
	return C;
}

void AddHead(LinkClause C){
	LinkClause p = C;
	while(p){
		LinkList cur = p->L;
		LinkList temp = new List;
		temp->num = 0;
		temp->next = p->L;
		p->L = temp;
		p = p->next;
	}
}

/***
	判断是否为空
***/

status IsNULL(LinkClause C){
	if(C->next == NULL){
		return TRUE;
	}
		LinkClause p = C->next;
		while(p){
			if(p->length!=0){
				return FALSE;
			}
			p = p->next;
		}
    return TRUE;
}

/***
	判断是否有空子句
***/

status IsEmptyList(LinkClause C){
	LinkClause p = C->next;
	if(p == NULL){
		return TRUE;
	}
	while(p){
		if(p->length == 0){
			return TRUE;
		}
		p = p->next;
	}
	return FALSE;
}


/***
	寻找单子句
***/

LinkClause FindSingleClause(LinkClause C){
	LinkClause p = C->next;
	while(p!= NULL){
		if(p->length == 1){
			return p;
		}
		p = p->next;
	}
	return NULL;
}

/***
删除子句
***/
LinkClause DeleteClause(LinkClause C,LinkClause cur){
	LinkClause q = C;
	LinkClause p = C->next;
	while(p){
		if(p == cur){
			q->next = cur->next;
			LinkList l = cur->L;
			while(l){
				LinkList temp = l;
				l = l->next;
				delete(temp);
			}
			delete(cur);
			break;
		}
		q = q->next;
		p = p->next;
	}
	C->length--;
	return q;
}

/***
头插法构造单子句
***/
LinkClause AddSingleClause(LinkClause C,int num){
	if(C == NULL){
		return NULL;
	}
	LinkClause p = C;
	LinkClause q = new Clause ;
	LinkList l = new List;
	LinkList t = new List;
	//进行赋值
	t->next = NULL;
	t->num = num;
	l->next = t;
	l->num = 0;
	q->length = 1;
	q->L = l;
	//开始链接
	q->next = p->next;
	p->next = q;
	C->length++;
	return C;
}

/***
	简化范式
***/
void SimplifyClause(LinkClause C,int num) {
	LinkClause p = C->next;
	LinkClause q = C;
	int flag = 0;
	while (p) {
		flag = 0;
		LinkList p1 = p->L;
		LinkList q1 = p1;
		p1 = p1->next;//此处p1可能为空，但是while会判断
		while (p1) {
			if (p1->num == num) {
				LinkList temp1 = p->L;
				LinkList temp2 = temp1->next;
				while (temp2) {
					temp1->next = temp2->next;
					delete(temp2);
					temp2 = temp1->next;
				}
				delete(temp1);
				q->next = p->next;
				p->L = NULL;
				delete(p);
				C->length--;
				p = q->next;
				flag = 1;
				break;
			}
			else if (p1->num == -num) {
				q1->next = p1->next;
				delete(p1);
				p->length--;
				p1 = q1->next;
				continue;
			}
			q1 = q1->next;
			p1 = p1->next;
		}
		if (flag == 0) {
			p= p->next;
			q = q->next;
		}
	}

}
/***
	删除含相同节点的子句，同时删除该变量
***/
void DeleteNode(LinkClause C,int num){
	LinkClause q = C;
	LinkClause p = C->next;
	while(p){
		l1:
		LinkList cur = p->L->next;
		LinkList pre = p->L;
		while(cur){
			if(cur->num == num){
				q = DeleteClause(C,p);
				p = q->next;
				if(p == NULL){
					return;
				}
				goto l1;
			}
			else if(abs(cur->num) == abs(num)){
				pre->next = cur->next;
				delete(cur);
				cur = pre->next;
				p->length--;
				continue;
			}
			pre = pre->next;
			cur = cur->next;
		}
		p = p->next;
		q = q->next;
		
	}
}

/***
创建副本
***/
LinkClause copy(LinkClause C){
		LinkClause p = C;
		LinkClause t = new Clause;
		t->length = C->length;
		t->L = replicate(p->L);
		t->next = NULL;
		LinkClause temp = t;
		while(p->next){
			t->length = p->length;
			t->L = replicate(p->L);
			t->next = new Clause;
			t = t->next;
			p = p->next;
		}
		t->L = replicate(p->L);
		t->length = p->length;
		t->next = NULL;
	return temp;
}


/***
尝试新的copy函数
***/

LinkClause AdvancedCopy(LinkClause C) {
	LinkClause p = new Clause;
	LinkClause q = C->next;
	p->L = new List;
	p->L->next = NULL;
	p->L->num = 0;
	p->length = C->length;
	p->next = NULL;
	LinkClause temp = p;
	//头节点初始化完成
	int i = 0;
	while (i < C->length) {
		p->next = new Clause;
		p = p->next;
		p->L = new List;
		p->L->next = NULL;
		p->L->num = 0;
		i++;
	}
	p->next = NULL;
	p = temp->next;
	while (q) {
		LinkList temp1 = q->L->next;
		LinkList temp2 = p->L;
		while (temp1) {
			temp2->next = new List;
			temp2 = temp2->next;
			temp2->next = NULL;
			temp2->num = temp1->num;
			temp1 = temp1->next;
		}
		temp2->next = NULL;
		p = p->next;
		q = q->next;
	}
	p = temp;
	q = C;
	while (q) {
		p->length = q->length;
		p = p->next;
		q = q->next;
	}
	return temp;


}

/***
赋值链表
***/
LinkList replicate(LinkList l){
	LinkList p = new List;
	p->num = 0;
	LinkList cur = l;
	if (l == NULL) {
		return NULL;
	}
	LinkList temp = p;
	while(cur->next){
		p->next = new List;
		p->num = cur->num;
		p = p->next;
		cur = cur->next;
	}
	p->num = cur->num;
	p->next = NULL;
	return temp;
}

//展示结果
void show(bool* result){
	for(int i = 0;i < VarN;i++){
		if(result[i] == true){
			printf("%d ",i+1);
		}
		else if(result[i] == false){
			printf("%d ",-(i+1));
		}
		else{
			printf("%d ",i+1);
		}
	}
}

//返回VarN的值
int returnN(){
	return VarN;
}

//Print
void Print(LinkClause C){
	LinkClause cur = C;
		while(cur!=NULL){
				LinkList temp = cur->L;
				printf("length == %d ",cur->length);
				while(temp!=NULL){
					printf("%d ",temp->num);
					temp = temp->next;
				}
			cur = cur->next;
			printf("\n");
		}
}

int SelectWord(LinkClause C) {
	LinkClause p = C->next;
	int min = 999;
	int temp = 0;
	while (p) {
		if (p->length < min) {
			min = p->length;
			temp = p->L->next->num;
		}
		p = p->next;
	}
	return temp;
}

status DPLL(LinkClause C,bool* result){
	LinkClause SingleClause = FindSingleClause(C);
	while(SingleClause!=NULL){
		int temp = SingleClause->L->next->num;
		temp > 0?result[temp-1] = true:result[abs(temp)-1] = false;
		DeleteClause(C,SingleClause);
		DeleteNode(C,temp);
		if(IsNULL(C)){
			return TRUE;
		}
		else if(IsEmptyList(C)){
			return FALSE;
		}
		SingleClause = FindSingleClause(C);
		//printf("%d\n", C->length);
	}
	int val = C->next->L->next->num;
	LinkClause replica = AdvancedCopy(C);
	LinkClause temp1 = AddSingleClause(C,val);
	//Print(temp1);
	if(DPLL(temp1,result)){
		return TRUE;
	}
	LinkClause temp2 = AddSingleClause(replica,-val);
	int t = DPLL(temp2,result);
	freeList(temp2);
	return t;

}

status AdvancedDPLL(LinkClause C, bool* result) {
	stack <LinkClause> s;
	LinkClause* ListL = new LinkClause[100000];
	for (int i = 0; i < 100000; i++) {
		ListL[i] = NULL;
	}
	int i = 0;//ListL用来记录每次改变的链表结点内容
	LinkClause temp = nullptr;
	int* v = new int[100000];
	int val = FALSE;
	s.push(C);
	//printf("C is in the stack!\n");
	while (!s.empty()) {
		//printf("entering while loop 2\n");
		while ((C = s.top()) && (val = SingleSpread(C, result)) == NORMAL) {
			//printf("ready to copy!\n");
			temp = AdvancedCopy(C);
			//printf("here is the copy\n");
			//Print(temp);
			ListL[i] = temp;
			//printf("temp in ListL\n");
			v[i] = C->next->L->next->num;
			//printf("selected word %d\n", v[i]);
			C = AddSingleClause(C, v[i]);
			s.push(C); i++;
			//printf("i = %d\n", i);
		}
		if (val == TRUE) {
			return TRUE;
		}
		s.pop();
		i--;
		//printf("ready to free\n");
		freeList(C);
		//printf("freed successful\n");
		if (!s.empty()) {
			C = ListL[i]; s.pop();
			//printf("push reverse %d", v[i]);
			s.push(AddSingleClause(C, -v[i]));
		}
	}
	delete[] ListL;
	delete[] v;
	return FALSE;

}
void freeList(LinkClause C) {
	if (C == NULL) {
		return;
	}
	LinkClause p = C;
	while (p) {
		LinkList q = p->L;
		while (q) {
			LinkList temp = q;
			q = q->next;
			//printf("delete %d\n", temp->num);
			delete(temp);
		}
		LinkClause temp2 = p;
		p = p->next;
		//printf("freed head\n");
		delete(temp2);
		
	}
}
int SingleSpread(LinkClause C,bool* result) {
	LinkClause SingleClause = FindSingleClause(C);
	while (SingleClause != NULL) {
		int temp = SingleClause->L->next->num;
		//printf("temp = %d\n",temp);
		temp > 0 ? result[temp - 1] = true : result[abs(temp) - 1] = false;
		//printf("ready to delete %d------------------------------\n", temp);
		//Print(C);
		SimplifyClause(C, temp);
		//Print(C);
		//printf("delete successful------------------------------------\n");
		//Print(C);
		if (IsNULL(C)) {
			//printf("True\n");
			return TRUE;
		}
		else if (IsEmptyList(C)) {
			//printf("False\n");
			return FALSE;
		}
		//Print(C);
		SingleClause = FindSingleClause(C);
	}
	//printf("Normal\n");
	return NORMAL;
}
void judge(char filename[],char suffix1[],char suffix2[]) {
	int sure = 0;
		//printf("VarN = %d\n", VarN);
		char read_file[100];
		char write_file[100];
		strcpy(read_file, filename);
		strcat(read_file, suffix1);
		printf("are you sure to read from %s?\n", read_file);
		printf("0 for no\n");
		scanf("%d", &sure);
		if (sure == 0) {
			exit(0);
		}
		sure = 1;
		strcpy(write_file, filename);
		strcat(write_file, suffix2);
		printf("are you sure to write to %s?\n", write_file);
		printf("0 for no\n");
		scanf("%d", &sure);
		if (sure == 0) {
			exit(0);
		}
		sure = 1;
		bool* result = new bool[10000];
		for (int i = 0; i < VarN; i++) {
			result[i] = true;
		}
		int begin = 0; int end = 0;
		int begin2 = 0; int end2 = 0;
		int option = 0;
		int original_time = 0;
		int optimized_time = 0;
			FILE* wp = fopen(write_file, "w");
		    LinkClause h = init(read_file);
			Print(h);
			begin = clock();
			int t = DPLL(h, result);
			end = clock();
			LinkClause h2 = init(read_file);
			Print(h2);
			begin2 = clock();
			int t2 = AdvancedDPLL(h2, result);
			end2 = clock();
			original_time = end - begin;
			optimized_time = end2 - begin2;
			printf("original: %d ms,from %d to %d\n", original_time,begin,end);
			printf("optimized: %d ms,from %d to %d\n", optimized_time,begin2,end2);
			printf("t = %d,t2 = %d\n", t, t2);
		if(t2&&t){
			show(result);
			printf("successful\n");
			fprintf(wp, "s 1\nv ");
			for (int i = 0; i < VarN; i++) {
				if (result[i] == true) {
					fprintf(wp,"%d ", i + 1);
				}
				else if (result[i] == false) {
					fprintf(wp,"%d ", -(i + 1));
				}
				else {
					fprintf(wp,"%d ", i + 1);
				}
			}
			fprintf(wp, "\n");
		}
		else{
			fprintf(wp, "s 0\n");
			printf("No solution\n");
		}
		fprintf(wp, "t\n");
		fprintf(wp, "original: %d ms\n", original_time);
		fprintf(wp, "optimized: %d ms\n", optimized_time);
		fprintf(wp, "optimize rate: %.2lf\%\n", (original_time - optimized_time) * 100.0 / original_time);
		delete []result;
		fclose(wp);
}
